Inference at * 1 1 1 1 
Iof proof for Lemma bool sq:



1. x : ?Unit
2. y : ?Unit
3. x = y
4. case x of inl(x) => x | inr(x) => x = case y of inl(x) => x | inr(x) => x
5. case x of inl(x) => True | inr(x) => False = case y of inl(x) => True | inr(x) => False
6. True = False
  False 

latex

 by ((RevHypSubst (-1) 0) 
CollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 4:n
C)) (first_tok :t) inil_term))) 

latex

C.

Definitions

t  T, True,